\section{M\'odulo Monopoly}

Servicios Exportados:

\subsubsection{Interfaz \nombretad{Monopoly}}


\textbf{g\'enero:} monopoly

\textbf{Usa interfaces:}
	\nombretad{Nat}, \nombretad{Bool}, \nombretad{DiccionarioT}, 
	\nombretad{Conjunto}, \nombretad{SecuenciaA}, \nombretad{SecuenciaL},
	\nombretad{Tupla}

\textbf{\bf se explica con especificacion:} \nombretad{Monopoly}

\vspace{0.5cm}
\textbf{Operaciones:}

\vspace{0.5cm}

\noindent
Nuevo(in t: tablero, in s: secu(jugador), in efectivoInicial: nat, in recompensa: nat) ret: mm \\
\{$  esCuadrado?(\sombrero{t}) \land 
	tienePrision(\sombrero{t}) \land
	 (long(\sombrero{s}) \geq 2) \land
	(\neg hayRepetidos?(\sombrero{s})) \land 
	(\sombrero{efectivoinicial} >  0) \land 
	(\sombrero{recompensa} > 0)  $\}
\\
\{$ \sombrero{ret} \igobs nuevo(\sombrero{t}, \sombrero{s}, \sombrero{e}, \sombrero{r}) $\}
\\

TirarDados(inout m: mm, in d: dados) \\
\{$ \sombrero{m} = m_0 \land \neg finalizado?(m_0) $\}\\
\{$ \sombrero{m} = siguienteJugada(m_0, \sombrero{d}) $\}\\

ComprarPropiedad(inout m: mm) \\
\{$ \sombrero{m} = m_0 \land puedeComprar?(m_0) $\}\\
\{$ \sombrero{m} = comprarPropiedad(m_0) $\}\\

Nuevo?(in m: mm) ret: bool \\
\{$ true $\}\\
\{$ \sombrero{ret} \igobs nuevo?(\sombrero{m}) $\}\\

Tablero(in m: mm) ret: tmm \\
\{$ true $\}\\
\{$ \sombrero{ret} \igobs tablero(\sombrero{m}) $\}\\

Jugadores(in m: mm) ret: secu(jugador) \\
\{$ true $\}\\
\{$ \sombrero{ret} \igobs jugadores(\sombrero{m}) $\}\\

Pr\'oximoTurno(in m: mm) ret: jugador \\
\{$ \neg finalizado?(\sombrero{m}) $\}\\
\{$ \sombrero{ret} \igobs proximoTurno(\sombrero{m}) $\}\\

EfectivoInicial(in m: mm) ret: nat \\
\{$ true $\}\\
\{$ \sombrero{ret} \igobs efectivoInicial(\sombrero{m}) $\}\\

Recompensa(in m: mm) ret: nat \\
\{$ true $\}\\
\{$ \sombrero{ret} \igobs recompensa(\sombrero{m}) $\}\\

Efectivo (in m: mm, j: jugador) ret: nat \\
\{$ esta?(\sombrero{m},\sombrero{j}) $\}\\
\{$ \sombrero{ret} \igobs efectivo(\sombrero{m},\sombrero{j}) $\}\\

Propiedades (in m: mm, j: jugador) ret: conj(nat) \\
\{$ esta?(\sombrero{m},\sombrero{j}) $\}\\
\{$ \sombrero{ret} \igobs propiedades(\sombrero{m},\sombrero{j}) $\}\\

EnPrisi\'on?(in m: mm, in j: jugador) ret: bool \\
\{$ esta?(\sombrero{m},\sombrero{j}) $\}\\
\{$ \sombrero{ret} \igobs enPrision?(\sombrero{m},\sombrero{j}) $\}\\

CantidadTurnosEnPrisi\'on(in m: mm, in j: jugador) ret: nat \\
\{$ esta?(\sombrero{m},\sombrero{j}) \land enPrision?(\sombrero{m}, \sombrero{j}) $\}\\
\{$ \sombrero{ret} \igobs \sharp turnosEnPrisi'on(\sombrero{m},\sombrero{j}) $\}\\

Termin\'o?(in m: mm) ret: bool \\
\{$ true $\}\\
\{$ \sombrero{ret} \igobs finalizado?(\sombrero{m}) $\}\\

Ganador(in m: mm) ret: jugador \\
\{$ finalizado?(\sombrero{m}) == true $\}\\
\{$ \sombrero{ret} \igobs ganador(\sombrero{m})  $\}\\

Due\~no (in m: mm, in p: nat) ret: jugador \\
\{$ \s{p} < \sharp casillas(tablero(\s{m})) \yluego 
 \big{(} \neg(esPrision(tablero(\s{m}),\s{p}) \lor 
	 esInicio?(tablero(\s{m}),\s{p})) \land 
	tieneDueno?(\s{m},\s{p})
\big{)}  $\}\\
\{$ esta?(\s{m},\s{ret}) \land (\s{p} \in propiedades(\s{m}, \s{ret})) $\}\\

\subsubsection{Aspectos de Aliasing}
Las siguientes funciones de este m\'odulo realizan aliasing: \\
\begin{itemize}
\item{blablabla}
\item{blobloblo}
\end{itemize}

\subsubsection{Ordenes de Complejidad}

\begin{itemize}
\item{blablabla}
\item{blobloblo}
\end{itemize}

\subsection{Representaci\'on}

\subsubsection{Estructura de Representaci\'on}

MiniMonopoly src {\bf estrM} donde {\bf estrM} es

< diccionarioT(nombre, <nat: efectivo x propiedades: conj(propiedad)> ) x
 ranking : secuL(jugador) x   % NO es un heap
 due\~nos : secuA(jugador) >

\subsubsection{Invariante de Representaci\'on}

Rep: $\sombrero{estrM}$ $\longrightarrow boolean $
$(\forall e: \sombrero{estrM})\,Rep(e) \equiv$

\begin{enumerate}
\item{blablabla}
\item{blobloblo}
\end{enumerate}

\vspace{0.5cm}

\subsubsection{Explicaciones del Invariante}
\begin{enumerate}
\item{blablabla}
\item{blobloblo}
\end{enumerate}

\vspace{0.3cm}

\subsubsection{Funci\'on de Abstracci\'on}

%($\forall$ $e$: $\sombrero{estrR}$) Abs($e$)  $\equiv$ $r$: $\sombrero{restaurant}$ {\bf tal que} 
%$\Big($  mozos($r$) $=$ claves($e$.DiccMozo)  $\wedge$ 
%mesas($r$) $=$ claves($e$.DiccMesas) $\wedge$ 
%recetario($r$) $=$ $e$.Recetario $\wedge$ 
%($\forall$ $i$: ingrediente) $\big($$i$ $\in$ ingredientes($r$) $\impluego$ stock($r$,$i$) $=$ obtener($i$,$e$.Stock)$\big)$  $\wedge$ 
%($\forall$ $m$: mesa) $\big($$m$ $\in$ mesas($r$) $\impluego$ 
%\indent mesaOcupada($r$,$m$) = $\big($obtener($m$, $e$.DiccMesa)$\big)$.ocupada $\wedge$  
%\indent mozoAsignado($r$,$m$) = $\big($obtener($m$, $e$.DiccMozo)$\big)$.mozo $\wedge$  
%\indent mesaocupada($r$,$m$) $\impluego$ $\big($pedidosPendientes($r$,$m$) = $\big($obtener($m$,$e$.DiccMesa$\big)$.pendientes $\big)$ $\Big)$

\subsubsection{Consideraciones sobre la elecci\'on de la estructura}
\vspace{0.2cm}
Teniendo en cuenta que  \textit{r: estrR} es nuestra estructura de representaci\'on, realizamos las siguientes consideraciones al elegir la estructura a utilizar: \\
\\
\textbf{Sobre la Estructura de Representaci\'on}
\begin{itemize}
\item{blablabla}
\item{blobloblo}
\end{itemize}

\vspace{0.5cm}

\subsection{Algoritmos}

%----------------------------------------------------------------------------------

%\begin{algorithm}{\it iPagar}{\param {in}{r}{restaurant}, \param{in}{m}{mesa}}{}
%		\VAR{datosMesa: DatosMesa} \\
%		datosMesa \= obtenerA(m, r.diccMesa) \\
%		datosMesa.ocupada \= false
%\end{algorithm}

%----------------------------------------------------------------------------------

%\begin{algorithm}{\it iSePuedePreparar}{\param {in}{r}{restaurant}, \param {in}{c}{multiconj(plato)}}{res\!:bool}
%	\VAR{ingredNecesarios: conj(ingrediente)} \\
%	\VAR{itIngred: iterConj(ingrediente)} \\
%	\VAR{ingredActual: ingrediente} \\
%	\\
%	res \= true \\
%	ingredNecesarios \= ingredientesNecesariosPedido(r.recetario, c) \\
%	itIngred \= crearIt(ingredNecesarios) \\
%	\\
%	\begin{WHILE}{tieneProximo(itIngred) \wedge res}
%		ingredActual \= proximo(itIngred) \\
%		\begin{IF}{cantidadNecesariaPedido(r.recetario, c, ingredActual) >  stock(r, ingredActual)}
%			res \= false
%		\end{IF}
%	\end{WHILE}
%\end{algorithm}


\subsubsection{Explicaci\'on de los \'ordenes de complejidad }

\begin{itemize}
\item{blablabla}
\item{blobloblo}
\end{itemize}

\subsection{Servicios Usados}
Para poder cumplir con los \'ordenes de complejidad requeridos, 
es necesario pedirle a los tipos usados los siguientes \'ordenes de complejidad para algunas funciones:

\subsubsection{\nombretad{Diccionario}}
Se requiere que las operaciones tengan los siguientes \'ordenes:
\begin{itemize}
\item Obtener: $O(1)$
\item Definir: $O(1)$
\end{itemize}

\subsubsection{\nombretad{Conjunto}}
Se requiere que las operaciones tengan los siguientes \'ordenes:
\begin{itemize}
\item Union: $O(1)$
\end{itemize}

\subsubsection{\nombretad{SecuenciaA}}
Se requiere que las operaciones tengan los siguientes \'ordenes:
\begin{itemize}
\item I\'esimo: $O(1)$
\end{itemize}

